A power series in a variable and with coefficients in a ring is a series of the form
where is in for each . Given that there are no additional convergence conditions, a power series is also termed emphatically as a formal power series. If is commutative, then the collection of formal power series in a variable with coefficients in forms a commutative ring denoted by .
More generally, a power series in commuting variables with coefficients in a ring has the form . If is commutative, then the collection of formal power series in commuting variables form a formal power series ring denoted by .
More generally, we can consider noncommutative (associative unital) ring and words in noncommutative variables of the form
(where has nothing to do with ) and with coefficient (here is a word of any length, not a multiindex in the previous sense). Thus the power sum is of the form and they form a formal power series ring in variables denoted by . Furthermore, can be even a noncommutative semiring in which case the words belong to the free monoid on the set , the partial sums are then belong to a monoid semiring . The formal power series then also form a semiring, by the multiplication rule
Of course, this implies that in a specialization, -s commute with variables ; what is usually generalized to take some endomorphisms into an account (like at noncommutative polynomial level of partial sums where we get skew-polynomial rings, i.e. iterated Ore extensions).
Let be a commutative ring, and let be the polynomial ring on one indeterminant . Then is a maximal ideal in , and results in an adic topology on . The ring of formal power series in is the adic completion of the limit of the quotient of by powers of :
The ring of formal power series for multiple indeterminants is constructed iteratively: because is a commutative ring, one could construct the polynomial ring on the indeterminant . As above, is a maximal ideal in with a corresponding adic topology, and one can then take the adic completion
The resulting commutative ring is usually just written as .
For a natural number , a power series such that for all is a polynomial of degree at most .
For a smooth function on the real line, and for denoting its th derivative its MacLaurin series (its Taylor series at ) is the power series
If this power series converges to , then we say that is analytic.
This follows easily from the observation that we can invert for any power series by forming and collecting only finitely many terms in each degree. As a simple corollary,
equipped with the ideal is the free adic -algebra on generators, in the sense that it is the value of the left adjoint to the forgetful functor
as applied to the set .
The idea is that for each adic -algebra and element , there is a unique adic algebra map that sends to ; this adic algebra map sends a power series to the sequence of truncations
belonging to .
It follows that we may define a clone or cartesian operad as follows: the component is the set which is the monad value . Letting denote the monad , with monad multiplication , and the set , the clone multiplication
is the composition of the maps
The clone multiplication thus defined is called substitution of power series; it takes a tuple consisting of to a power series denoted as
The resulting clone or operad yields, in the particular case , an associative substitution operation
with the power series .
The group of invertible elements in the substitution monoid consists of power series of the form where is multiplicatively invertible in the ring .
In other words, we can functionally invert a power series provided that the linear coefficient is invertible in .
Given power series and , we may read off coefficients of the composite as
where in particular . Now is the left functional inverse of , or is the right inverse of , if , i.e., if if and otherwise. The first equation says simply which implies is invertible. Conversely, if is multiplicatively invertible and , then the equations
may be uniquely solved for the remaining 's given the 's, and uniquely solved for the remaining 's given the 's, by an inductive procedure: for we have
and this allows us to solve for ,
given the values and earlier -values for given by inductive hypothesis. Similarly we can solve for in terms of given coefficients and earlier -values , . Thus every power series has a right inverse if exists, and has a left inverse if exists, and this completes the proof.
One way to define the formal differentiation operator, as a function , is via the usual formula
Then is an -linear function on which satisfies the Leibniz rule, meaning that it is a derivation and is a differential algebra.
Here is a conceptual story underlying the formalism. Let be the representing object for derivations (the “ring of dual numbers”). Let be the unique topological -algebra map (under the -adic topologies described above) that sends to . (If it helps, think .)
For , the derivative is the unique element of satisfying
We leave as an exercise the proof that the two definitions of derivative match:
(Hint: the restriction of to is by construction a derivation such that , and by induction. This induces derivations on quotient algebras , satisfying the same formula. Then pass to the inverse limit.)
(Chain rule) For and ,
See here for a conceptual proof, using the universal property of adic completion.
Relatedly but in a slightly different direction, we can consider differentiation in coalgebraic terms. Suppose the commutative ring is a commutative algebra over (thus permitting division by nonzero integers). Then the set may be identified with the terminal coalgebra of the endofunctor via the map
whereby the coalgebra structure on ,
corresponds to
One may then apply coinductive techniques to prove various facts. One illustration is given here, where coinduction on power series is used to prove the general binomial theorem
where, remarkably, is an arbitrary element of .
ring with infinitesimals | function |
---|---|
dual numbers | differentiable function |
Weil ring | smooth function |
power series ring | analytic function |
Suppose that is a Archimedean ordered field and is the ring of power series in . Since is a local ring, the quotient of by its ideal of non-invertible elements is the residue field itself, and the canonical function used in defining the quotient is the function which takes a number to its purely real component and takes . Since is an ordered -algebra, there is a strictly monotone ring homomorphism . An element is purely real if , and an element is purely infinitesimal if it is in the fiber of at . Zero is the only element in which is both purely real and purely infinitesimal.
Suppose that is a sequentially Cauchy complete Archimedean ordered field with lattice structure, and is the ring of power series of . Then analytic functions are each definable on using the algebraic, order, metric, and convergence structure on .
The ring homomorphism preserves analytic functions: given a natural number and a purely infinitesimal element , then for every analytic function , there is a function such that for all elements , and
A formalization in homotopy type theory and there in Coq is discussed in section 4 of
The discussion of the differentiation of a converging power series term by term is at
Last revised on August 19, 2024 at 15:03:52. See the history of this page for a list of all contributions to it.